E:Type, pred?:(E(E+Unit)), info:(E(IdId+(IdLnkE)Id)), V:(IdIdType), M:(IdLnkIdType),
T:(IdIdType), init:(i,x:IdT(i,x)),
Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x))),
Choose:(i,a:Id(x:IdT(i,x))(V(i,a)+Unit)),
Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List)),
val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) )).
(e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 SWellFounded(pred!(e;e'))
 val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val)  Prop 

latex

Definitions

False, b, islocal(k), rcv(l,tg), t  T, {T}, P  Q, x:A. B(x), SQType(T), Knd, Prop, s ~ t, kind(e), tag(k), lnk(k), A, b, , x:AB(x), P & Q, P  Q, Unit, kindcase(k; a.f(a); l,t.g(l;t) ), Type, act(k), loc(e), <a,b>, Msg(M), True, isrcv(k), locl(a), ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv?(e), S  T, inr(x), state_when(e), isl(x), x,y. t(x;y), x. t(x), type List, pred(e), first(e), pred!(e;e'), SWellFounded(R(x;y)), sender(e), (x  l), outl(x), A & B, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), f(a), Id, IdLnk, x:AB(x), left+right, s = t

Lemmas

outl wf, isrcv wf, l member wf, sender wf, strongwellfounded wf, pred! wf, first wf, pred wf, Msg wf, kindcase wf, isl wf, unit wf, state when wf, IdLnk wf, false wf, true wf, loc wf, Id wf, actof wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, islocal wf, bool wf, bnot wf, not wf, assert wf, subtype rel self, lnk wf, tagof wf, isrcv-implies, kind wf, Knd wf, Knd sq